{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : $Header$

Description : prenex normal form for sentences of a CASL theory

Copyright : (c) Mihai Codescu, 2016

License : GPLv2 or higher, see LICENSE.txt

Maintainer : codescu@iws.cs.uni-magdeburg.de

Stability : provisional

Portability : non-portable (imports Logic.Comorphism)

-}

module Comorphisms.CASL2Prenex where

import Logic.Logic

import Logic.Comorphism

import CASL.Logic_CASL

import CASL.AS_Basic_CASL

import CASL.Sign

import CASL.Morphism

import CASL.Sublogic as SL hiding (bottom)

import CASL.Induction

import CASL.Quantification

import Common.Result

import Common.Id

import qualified Data.Set as Set

import Common.AS_Annotation

import Common.ProofTree

data CASL2Prenex = CASL2Prenex deriving Show

instance Language CASL2Prenex where

language_name CASL2Prenex = "CASL2Prenex"

instance Comorphism CASL2Prenex

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree where

sourceLogic CASL2Prenex = CASL

sourceSublogic CASL2Prenex = SL.caslTop

targetLogic CASL2Prenex = CASL

mapSublogic CASL2Prenex sl =

Just $ min sl (sl{SL.which_logic = SL.Prenex})

map_theory CASL2Prenex = mapTheory

map_morphism CASL2Prenex = return

map_sentence CASL2Prenex sig = return . (mapSentence sig)

map_symbol CASL2Prenex _ = Set.singleton . id

has_model_expansion CASL2Prenex = True

is_weakly_amalgamable CASL2Prenex = True

-- remove equivalences

preprocessSen :: CASLFORMULA -> CASLFORMULA

preprocessSen sen = case sen of

Quantification q vdecls sen' r ->

Quantification q vdecls (preprocessSen sen') r

Junction j sens r ->

Junction j (map preprocessSen sens) r

Relation sen1 Equivalence sen2 _ -> let

sen1' = Relation sen1 Implication sen2 nullRange

sen2' = Relation sen2 Implication sen1 nullRange

in Junction Con [sen1', sen2'] nullRange

Relation sen1 rel sen2 r ->

Relation (preprocessSen sen1) rel

(preprocessSen sen2) r

Negation sen' r ->

Negation (preprocessSen sen') r

_ -> sen

-- make variables distinct:

-- if a variable v of sort s already appears in a formula

-- substitute it with a fresh variable

mkDistVars :: CASLFORMULA -> CASLFORMULA

mkDistVars sen =

let (_, _, sen') = mkDistVarsAux 0 [] sen

in sen'

mkDistVarsAux :: Int -- first available suffix for vars

-> [(VAR, SORT)] -- vars encountered so far

-> CASLFORMULA

-> (Int, [(VAR, SORT)], CASLFORMULA)

mkDistVarsAux n vlist sen = case sen of

Quantification q vdecls form range -> let

-- first make variables distinct for form

dvars = flatVAR_DECLs vdecls

(n', _, form') = mkDistVarsAux n (dvars ++ vlist) form

-- here we are not interested in the variables generated for the quantified form, so we can forget them

replVarDecl vds oN nN s = reverse $

foldl (\usedD vd@(Var_decl names sort r) ->

if sort == s then -- found it, replace oN with nN in names

let vd' = Var_decl (map (\x -> if x == oN then nN else x) names) sort r

in vd':usedD

else vd:usedD

) [] vds

checkAndReplace (n0, knownV, quantF, quants) (x, s) =

if (x,s) `elem` knownV

then

let

x' = genNumVar "x" n0

quants' = replVarDecl quants x x' s

quantF' = substitute x s (Qual_var x' s nullRange) quantF

in (n0 + 1, (x', s):knownV, quantF', quants')

else (n0 , (x , s):knownV, quantF , quants )

(n'', vlist', form'', vdecls') = foldl checkAndReplace (n', vlist, form', vdecls) dvars

in (n'', vlist', Quantification q vdecls' form'' range)

Junction j sens r -> let

(n', vlist', sens') = foldl (\(x, vs, osens) s ->

let

(x', vs', s') = mkDistVarsAux x vs s

in (x', vs', s':osens)) (n, vlist, []) sens

in (n', vlist', Junction j (reverse sens') r)

Relation sen1 rel sen2 r -> let

(n1, vlist1, sen1') = mkDistVarsAux n vlist sen1

(n2, vlist2, sen2') = mkDistVarsAux n1 vlist1 sen2

in (n2, vlist2, Relation sen1' rel sen2' r)

Negation sen' r -> let

(n', vlist', sen'') = mkDistVarsAux n vlist sen'

in (n', vlist', Negation sen'' r)

_ -> (n, vlist, sen)

computePNF :: CASLFORMULA -> CASLFORMULA

computePNF sen = case sen of

Negation nsen _ -> let

nsen' = computePNF nsen

in case nsen' of

Quantification q vdecls qsen _ ->

Quantification (dualQuant q) vdecls

(computePNF $ Negation qsen nullRange) nullRange

_ -> Negation nsen' nullRange

Relation sen1 Implication sen2 _ -> let

sen1' = computePNF sen1

sen2' = computePNF sen2

in case sen1' of

Quantification q vdecls qsen _ ->

Quantification (dualQuant q) vdecls (computePNF $ Relation qsen Implication sen2 nullRange) nullRange

_ -> case sen2' of

Quantification q vdecls qsen _ ->

Quantification q vdecls

(computePNF $ Relation sen1' Implication qsen nullRange) nullRange

-- recursive call to catch multiple quantifiers for sen2'

_ -> -- no quantifications

Relation sen1' Implication sen2' nullRange

Relation sen1 RevImpl sen2 _ ->

computePNF $ Relation sen2 Implication sen1 nullRange

Quantification q vdecls qsen _ ->

Quantification q vdecls (computePNF qsen) nullRange

Junction j sens _ -> let

sens' = map computePNF sens

(vdecls, sens'') = foldl (\(vs, ss) s -> case s of

Quantification q vd' qs' _ -> ((q,vd'):vs, qs':ss)

_ -> (vs, s:ss))

([], []) sens'

qsen = Junction j (reverse sens'') nullRange

rsen = foldl (\s (q, vd) -> Quantification q vd s nullRange) qsen vdecls

in rsen

_ -> sen

mapSentence :: CASLSign -> CASLFORMULA -> CASLFORMULA

mapSentence _ =

computePNF . mkDistVars . preprocessSen

mapTheory :: (CASLSign, [Named CASLFORMULA]) ->

Result (CASLSign, [Named CASLFORMULA])

mapTheory (sig, nsens) = do

let nsens' = map (\nsen -> nsen{

sentence = mapSentence sig $ sentence nsen

})

nsens

return (sig, nsens')