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

{- |

Module : $Header$

Description : skolemization as an institution comorphism

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)

removing existential quantifiers from every formula

follows http://resources.mpi-inf.mpg.de/departments/rg1/teaching/autrea-ss10/script/lecture10.pdf

-}

module Comorphisms.CASL2Skolem 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

import qualified Common.Lib.MapSet as MapSet

import qualified Common.Lib.Rel as Rel

import Data.List(partition)

data CASL2Skolem = CASL2Skolem deriving Show

instance Language CASL2Skolem where

language_name CASL2Skolem = "CASL2Skolem"

instance Comorphism CASL2Skolem

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 CASL2Skolem = CASL

sourceSublogic CASL2Skolem = SL.cPrenex

targetLogic CASL2Skolem = CASL

mapSublogic CASL2Skolem sl = Just sl

map_theory CASL2Skolem = mapTheory

map_morphism CASL2Skolem = error "nyi"

map_sentence CASL2Skolem = mapSentence

map_symbol CASL2Skolem _ = Set.singleton . id

has_model_expansion CASL2Skolem = True

is_weakly_amalgamable CASL2Skolem = True

eps CASL2Skolem = False

mapSentence :: CASLSign -> CASLFORMULA -> Result CASLFORMULA

mapSentence sig sen = do

let (_n', _nsig', sen1) = skolemize 0 [] sig sig

$ miniscoping sig sen

return sen1

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

Result (CASLSign, [Named CASLFORMULA])

mapTheory (sig, nsens) = do

let (_, nsig, nsens') = foldl (\(n, nsig0, sens0) nsen ->

let (n', nsig', sen1) = skolemize n [] sig nsig0

$ miniscoping sig $ sentence nsen

in (n', nsig', nsen{sentence = sen1}:sens0))

(0, emptySign (), []) nsens

sig' = uniteCASLSign sig nsig

return (sig', reverse nsens')

mkSkolemFunction :: Int -> Id

mkSkolemFunction x =

genName $ "sk_f" ++ show x

-- replace each variable from an argument list vars

-- in a sentence sen'

-- with a new skolem function of arguments in a list fVars

-- the names are generated starting with a given number

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

(CASLSign, CASLFORMULA)

replaceBoundVars vars fVars n sen = let

-- for each variable that occurs free in sen,

-- generate a new skolem function name

fNames = map (mkSkolemFunction . snd) $ zip fVars $ [n..]

-- for each such name, its arguments will be the types of vars

-- and the result, the corresponding sort in fVars

otypes = map (\x -> Op_type Total (map snd vars) x nullRange) $

map snd fVars

-- now create the operation symbols with names in fNames and arity in otypes

osyms = map (\(x, y) -> Qual_op_name x y nullRange) $

zip fNames otypes

-- the arguments are the outer variables

args = map (\(v,s) -> Qual_var v s nullRange) vars

-- now create the term gn_sk_k(outerVariables)

tms = map (\os -> Application os args nullRange) osyms

substs = map (\((a,b),c) -> (a,b,c)) $ zip fVars tms

sen' = foldl (\f (v,s,t)-> substitute v s t f) sen substs

sign' = (emptySign ()) {

sortRel = foldl (\r x -> Rel.insertKey x r) Rel.empty $

map snd $ vars ++ fVars,

opMap = foldl (\m (f,o) -> MapSet.insert f (toOpType o) m)

MapSet.empty $ zip fNames otypes

}

in (sign', sen')

-- skolemization:

-- exists x H =>

-- H(f(y_1,...,y_n)/x)

-- where y_1, ..., y_n are free in exists x H

-- f is a new function symbol of arity n

skolemize :: Int -> [(VAR, SORT)] -> CASLSign -> CASLSign -> CASLFORMULA ->

(Int, CASLSign, CASLFORMULA)

skolemize n outerFreeVars osig nsig sen = case sen of

Quantification Existential vdecls sen1 _ -> let

vars = flatVAR_DECLs vdecls

(n', nsig', sen') = skolemize n outerFreeVars osig nsig sen1

--fVars = freeVars osig sen'

n'' = n' + (length vars)

(nsig0, sen'') = replaceBoundVars outerFreeVars vars n sen'

nsig'' = uniteCASLSign nsig' nsig0

in (n'', nsig'', sen'')

Quantification q vars sen1 _ ->

let (n', nsig', sen') = skolemize n (outerFreeVars ++ flatVAR_DECLs vars)

osig nsig sen1

in (n', nsig', Quantification q vars sen' nullRange)

Junction j sens _ -> let

(n', nsig', sens') = foldl (\(x, nsig0, sens0) s ->

let (y, nsig1, s') = skolemize x outerFreeVars osig nsig0 s

in (y, uniteCASLSign nsig1 nsig0, s':sens0))

(n, nsig, []) sens

in (n', nsig', Junction j sens' nullRange)

Relation sen1 rel sen2 _ -> let

(n', nsig', sen') = skolemize n outerFreeVars osig nsig sen1

(n'', nsig'', sen'') = skolemize n' outerFreeVars osig nsig' sen2

in (n'', nsig'', Relation sen' rel sen'' nullRange)

Negation sen1 _ ->

let (n', nsig', sen') = skolemize n outerFreeVars osig nsig sen1

in (n', nsig', Negation sen' nullRange)

x -> (n, nsig, x)

-- miniscoping:

-- Qx(G and F) => QxG and F

-- Qx(G or F) => QxG or F

-- forall x (G and H) => (forall x G) and (forall x H)

-- exists x (G or H) => (exists x G) or (exists x H)

-- where x occurs freely in G, H

-- but not in F

miniscoping :: CASLSign -> CASLFORMULA -> CASLFORMULA

miniscoping sig sen = case sen of

Quantification q vdecls (Junction j sens _) _ ->

let

vars = Set.fromList $ flatVAR_DECLs vdecls

(sensVarsFree, sensNoVars) = partition

(\s ->

let svars = freeVars sig s

in (svars /= Set.difference svars vars))

sens

sensVarsFree' = map (miniscoping sig) sensVarsFree

sensNoVars' = map (miniscoping sig) sensNoVars

in case (q, j) of

(Existential, Con) ->

Junction Con

((Quantification Existential vdecls

(Junction Con sensVarsFree' nullRange) nullRange)

: sensNoVars')

nullRange

(Existential, Dis) ->

Junction Dis

((map (\s -> Quantification Existential vdecls s nullRange)

sensVarsFree') ++ sensNoVars')

nullRange

(Universal, Con) ->

Junction Con

((map (\s -> Quantification Universal vdecls s nullRange)

sensVarsFree') ++ sensNoVars') nullRange

(Universal, Dis) ->

Junction Dis

((Quantification Universal vdecls

(Junction Dis sensVarsFree' nullRange) nullRange):sensNoVars')

nullRange

_ -> error "miniscoping nyi for exists uniquely"

Quantification q vdecls qsen _ ->

Quantification q vdecls (miniscoping sig qsen) nullRange

Junction j sens _ ->

Junction j (map (miniscoping sig) sens) nullRange

Relation sen1 rel sen2 _ ->

Relation (miniscoping sig sen1) rel (miniscoping sig sen2) nullRange

Negation nsen _ ->

Negation (miniscoping sig nsen) nullRange

x -> x