content: {-# 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)
  
  