{-# 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

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 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 $ 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 (reverse 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)

