{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2VSERefine.hs
Description :  VSE refinement as comorphism
Copyright   :  (c) M. Codescu, DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Mihai.Codescu@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from CASL to VSE.
-}

module Comorphisms.CASL2VSERefine (CASL2VSERefine (..)) where

import Logic.Logic
import Logic.Comorphism

import CASL.Logic_CASL
import CASL.Sublogic as SL
import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.Morphism

import VSE.Logic_VSE
import VSE.As
import VSE.Ana

import Common.AS_Annotation
import Common.Id
import Common.ProofTree
import Common.Result
import Common.Utils (number)
import Common.Lib.State
import qualified Common.Lib.MapSet as MapSet

import qualified Data.Set as Set
import qualified Data.Map as Map

-- | The identity of the comorphism
data CASL2VSERefine = CASL2VSERefine deriving (Show)

instance Language CASL2VSERefine -- default definition is okay

instance Comorphism CASL2VSERefine
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               VSE ()
               VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS
               VSESign
               VSEMor
               Symbol RawSymbol () where
    sourceLogic CASL2VSERefine = CASL
    sourceSublogic CASL2VSERefine = SL.cFol
    targetLogic CASL2VSERefine = VSE
    mapSublogic CASL2VSERefine _ = Just ()
    map_theory CASL2VSERefine = mapCASLTheory
    map_morphism CASL2VSERefine = return . mapMor
    map_sentence CASL2VSERefine _ = error "map sen nyi" -- return. mapCASSen
    map_symbol CASL2VSERefine = error "map symbol nyi"
    has_model_expansion CASL2VSERefine = True
        -- check these 3, but should be fine
    is_weakly_amalgamable CASL2VSERefine = True
    isInclusionComorphism CASL2VSERefine = False

mapCASLTheory :: (CASLSign, [Named CASLFORMULA]) ->
                 Result (VSESign, [Named Sentence])
mapCASLTheory (sig, n_sens) =
  let (tsig, genAx) = mapSig sig
      tsens = map mapNamedSen n_sens
      allSens = tsens ++ genAx
  in if null $ checkCases tsig allSens then return (tsig, allSens) else
     fail "case error in signature"

mapSig :: CASLSign -> (VSESign, [Named Sentence])
mapSig sign =
 let wrapSort (procsym, axs) s = let
        restrName = gnRestrName s
        eqName = gnEqName s
        sProcs = [(restrName, Profile [Procparam In s] Nothing),
                   (eqName,
                     Profile [Procparam In s, Procparam In s]
                             (Just uBoolean))]
        varx = Qual_var (genToken "x") s nullRange
        vary = Qual_var (genToken "y") s nullRange
        varz = Qual_var (genToken "z") s nullRange
        varb = Qual_var (genToken "b")
                        uBoolean nullRange
        varb1 = Qual_var (genToken "b1")
                        uBoolean nullRange
        varb2 = Qual_var (genToken "b2")
                        uBoolean nullRange
        sSens = [ makeNamed ("ga_termination_eq_" ++ show s) $
                  Quantification Universal [Var_decl [genToken "x",
                                                      genToken "y"] s nullRange
                                           , Var_decl [genToken "b"]
                                              uBoolean nullRange]
                  (mkImpl
                  (conjunct [
                   ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Call
                          (Predication (Qual_pred_name restrName
                                         (Pred_type [s] nullRange) nullRange)
                            [varx] nullRange))
                          nullRange)
                      trueForm ) nullRange,
                   ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Call
                          (Predication (Qual_pred_name restrName
                                         (Pred_type [s] nullRange) nullRange)
                            [vary] nullRange))
                          nullRange)
                      trueForm ) nullRange
                   ])
                  (ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                         (Assign (genToken "b")
                          (Application
                             (Qual_op_name
                               (gnEqName s)
                               (Op_type Partial [s, s] uBoolean nullRange)
                              nullRange)
                             [varx, vary] nullRange))
                          nullRange)
                      trueForm ) nullRange)
                  ) nullRange ,
                  makeNamed ("ga_refl_eq_" ++ show s) $
                  Quantification Universal [Var_decl [genToken "x"] s nullRange
                                           , Var_decl [genToken "b"]
                                              uBoolean nullRange]
                  (mkImpl
                  (ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Call
                          (Predication (Qual_pred_name restrName
                                          (Pred_type [s] nullRange ) nullRange)
                            [varx] nullRange))
                          nullRange)
                      trueForm ) nullRange)

                     (ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Assign (genToken "b")
                          (Application
                             (Qual_op_name
                               (gnEqName s)
                               (Op_type Partial [s, s] uBoolean nullRange)
                              nullRange)
                             [varx, varx] nullRange))
                        nullRange)
                      (mkStEq
                         varb
                         (Application (Qual_op_name uTrue
                                          (Op_type Total []
                                            uBoolean
                                           nullRange) nullRange)
                          [] nullRange)
                      )) nullRange)
                  ) nullRange
                 , makeNamed ("ga_sym_eq_" ++ show s) $
                  Quantification Universal [Var_decl [genToken "x",
                                                      genToken "y"] s nullRange
                                           , Var_decl [genToken "b1",
                                                      genToken "b2"]
                                              uBoolean nullRange]
                  (mkImpl
                   (conjunct [
                   ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Call
                          (Predication (Qual_pred_name restrName
                                         (Pred_type [s] nullRange) nullRange)
                            [varx] nullRange))
                          nullRange)
                      trueForm ) nullRange,
                   ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Call
                          (Predication (Qual_pred_name restrName
                                         (Pred_type [s] nullRange) nullRange)
                            [vary] nullRange))
                          nullRange)
                      trueForm ) nullRange,
                    ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Assign (genToken "b1")
                          (Application
                             (Qual_op_name
                               (gnEqName s)
                               (Op_type Partial [s, s] uBoolean nullRange)
                              nullRange)
                             [varx, vary] nullRange))
                          nullRange)
                      (mkStEq varb1 aTrue)
                     ) nullRange
                   ])
                     (ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Assign (genToken "b2")
                          (Application
                             (Qual_op_name
                               (gnEqName s)
                               (Op_type Partial [s, s] uBoolean nullRange)
                              nullRange)
                             [vary, varx] nullRange))
                          nullRange)
                      (mkStEq varb2 aTrue)
                     ) nullRange)
                  ) nullRange
                  , makeNamed ("ga_trans_eq_" ++ show s) $
                  Quantification Universal [Var_decl [genToken "x",
                                                      genToken "y",
                                                      genToken "z"] s nullRange
                                           , Var_decl [genToken "b1",
                                                      genToken "b2",
                                                      genToken "b"]
                                              uBoolean nullRange]
                  (mkImpl
                   (conjunct [
                   ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Call
                          (Predication (Qual_pred_name restrName
                                        (Pred_type [s] nullRange) nullRange)
                            [varx] nullRange))
                          nullRange)
                      trueForm ) nullRange,
                   ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Call
                          (Predication (Qual_pred_name restrName
                                        (Pred_type [s] nullRange ) nullRange)
                            [vary] nullRange))
                          nullRange)
                      trueForm ) nullRange,
                   ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Call
                          (Predication (Qual_pred_name restrName
                                        (Pred_type [s] nullRange ) nullRange)
                            [varz] nullRange))
                          nullRange)
                      trueForm ) nullRange,
                    ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Assign (genToken "b1")
                          (Application
                             (Qual_op_name
                               (gnEqName s)
                               (Op_type Partial [s, s] uBoolean nullRange)
                              nullRange)
                             [varx, vary] nullRange))
                          nullRange)
                      (mkStEq varb1 aTrue)
                      ) nullRange,
                    ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Assign (genToken "b2")
                          (Application
                             (Qual_op_name
                               (gnEqName s)
                               (Op_type Partial [s, s] uBoolean nullRange)
                              nullRange)
                             [vary, varz] nullRange))
                          nullRange)
                      (mkStEq varb2 aTrue)
                     ) nullRange
                   ])
                     (ExtFORMULA $ Ranged
                     (Dlformula Diamond
                      (Ranged
                        (Assign (genToken "b")
                          (Application
                             (Qual_op_name
                               (gnEqName s)
                               (Op_type Partial [s, s] uBoolean nullRange)
                              nullRange)
                             [varx, varz] nullRange))
                          nullRange)
                      (mkStEq varb aTrue)
                     ) nullRange)
                  ) nullRange ]
                                          in
        (sProcs ++ procsym, sSens ++ axs)
     (sortProcs, sortSens) = foldl wrapSort ([], []) $
                                        Set.toList $ sortSet sign
     wrapOp (procsym, axs) (i, opTypes) = let
       funName = mkGenName i
       fProcs = map (\ profile ->
                       (funName,
                        Profile
                           (map (Procparam In) $ opArgs profile)
                           (Just $ opRes profile))) opTypes
       opTypeSens (OpType _ w s) = let
          xtokens = map (\ (_, ii) -> genNumVar "x" ii) $
                    number w
          xvars = map (
                  \ (si, ii) ->
                  Qual_var (genNumVar "x" ii )
                  si nullRange ) $
                   number w
          yvars = map (
                  \ (si, ii) ->
                  Qual_var (genNumVar "y" ii )
                  si nullRange ) $
                   number w
          ytokens = map (\ (_, ii) -> genNumVar "y" ii) $
                    number w
          btokens = map (\ (_, ii) -> genNumVar "b" ii) $
                    number w
          xtoken = genToken "x"
          ytoken = genToken "y"
          btoken = genToken "b"
          xvar = Qual_var (genToken "x")
                  s nullRange
          yvar = Qual_var (genToken "y")
                  s nullRange
          bvar = Qual_var (genToken "b")
                  uBoolean nullRange
          congrF = [makeNamed "" $
                  Quantification Universal ([Var_decl [xtoken, ytoken] s
                                            nullRange
                                           , Var_decl (btoken : btokens)
                                              uBoolean nullRange
                                            ] ++ map
                                            (\ ((t1, t2), si) ->
                                             Var_decl [t1, t2] si
                                             nullRange)
                                             (zip (zip xtokens ytokens) w)
                                            )
               (mkImpl
                  (conjunct
                   (concatMap (\ (si, ii) -> let
                     xv = Qual_var (genNumVar "x" ii)
                           si nullRange
                     yv = Qual_var (genNumVar "y" ii)
                           si nullRange
                     varbi = genNumVar "b" ii
                     bi1 = Qual_var (genNumVar "b" ii)
                            uBoolean nullRange
                                          in
                     [ExtFORMULA $ Ranged ( Dlformula Diamond
                          (Ranged
                                (Call
                                 (Predication
                                   (Qual_pred_name
                                    (gnRestrName si)
                                    (Pred_type [si] nullRange) nullRange )
                                   [xv] nullRange))
                               nullRange)
                          trueForm ) nullRange ,
                       ExtFORMULA $ Ranged ( Dlformula Diamond
                              (Ranged
                                (Call
                                 (Predication
                                   (Qual_pred_name
                                    (gnRestrName si)
                                    (Pred_type [si] nullRange) nullRange)
                                   [yv] nullRange))
                               nullRange)
                          trueForm ) nullRange ,
                       ExtFORMULA $ mkRanged $ Dlformula Diamond
                              (Ranged
                                (Assign varbi
                            (Application
                             (Qual_op_name
                               (gnEqName si)
                               (Op_type Partial [si, si] uBoolean nullRange)
                              nullRange)
                             [xv, yv] nullRange))
                                nullRange)
                              (mkStEq bi1 aTrue)
                     ] ) $
                    number w )
                   ) -- hypothesis
                  (ExtFORMULA $ Ranged (
                     Dlformula Diamond

                      (Ranged
                        (Assign (genToken "x")
                            (Application
                             (Qual_op_name
                               (mkGenName i)
                               (Op_type Partial w s nullRange)
                              nullRange)
                             xvars nullRange))
                       nullRange)
                      (ExtFORMULA $ Ranged (
                         Dlformula Diamond
                      (Ranged
                         (Assign (genToken "y")
                            (Application
                             (Qual_op_name
                               (mkGenName i)
                               (Op_type Partial w s nullRange)
                              nullRange)
                             yvars nullRange))
                       nullRange)
                       (ExtFORMULA $
                        Ranged (
                          Dlformula Diamond
                          ( Ranged
                            (Assign (genToken "b")
                            (Application
                             (Qual_op_name
                               (gnEqName s)
                               (Op_type Partial [s, s] uBoolean nullRange)
                              nullRange)
                             [xvar, yvar] nullRange))
                          nullRange
                          )
                          (mkStEq bvar aTrue)
                        ) nullRange)
                        ) nullRange)
                   ) nullRange) -- conclusion
                  )
               nullRange
              ]
          termF = if not $ null w then
                   [ makeNamed "" $ Quantification Universal
                     (Var_decl [xtoken] s nullRange
                      : map (\ (t1, si) -> Var_decl [t1] si nullRange)
                        (zip xtokens w))
                     (mkImpl
                        (conjunct
                         (concatMap (\ (si, ii) -> let
                     xv = Qual_var (genNumVar "x" ii) si nullRange in
                     [ExtFORMULA $ Ranged ( Dlformula Diamond
                          (Ranged
                                (Call
                                 (Predication
                                   (Qual_pred_name
                                    (gnRestrName si)
                                    (Pred_type (w ++ [s]) nullRange) nullRange)
                                   [xv] nullRange))
                               nullRange)
                          trueForm ) nullRange
                     ] ) $
                    number w )
                        )
                        (ExtFORMULA $ Ranged
                       (
                       Dlformula Diamond
                       (Ranged
                         (Assign (genToken "x")
                            (Application
                             (Qual_op_name
                               (mkGenName i)
                               (Op_type Partial w s nullRange)
                              nullRange)
                             xvars nullRange))
                        nullRange)
                       (ExtFORMULA $
                         Ranged
                         (Dlformula Diamond (Ranged
                          (Call (Predication (Qual_pred_name
                                              (gnRestrName s)
                                    (Pred_type [s] nullRange) nullRange)
                              [xvar] nullRange))
                                             nullRange)
                          trueForm
                          )
                         nullRange)
                       ) nullRange)
                       )
                     nullRange
                   ]
                  else
                   [makeNamed "" $ Quantification Universal
                                   [Var_decl [xtoken] s nullRange]
                     (ExtFORMULA $ Ranged
                       (
                       Dlformula Diamond
                       (Ranged
                         (Assign (genToken "x")
                            (Application
                             (Qual_op_name
                               (mkGenName i)
                               (Op_type Partial [] s nullRange)
                              nullRange)
                             [] nullRange))
                        nullRange)
                       (ExtFORMULA $
                         Ranged
                         (Dlformula Diamond (Ranged
                          (Call (Predication (Qual_pred_name
                                              (gnRestrName s)
                                    (Pred_type [s] nullRange) nullRange)
                              [xvar] nullRange))
                                             nullRange)
                          trueForm
                          )
                         nullRange)
                       ) nullRange) nullRange]
                                   in
         if null w then termF else congrF ++ termF

       fSens = concatMap opTypeSens opTypes
                                            in
       (procsym ++ fProcs, axs ++ fSens)
     (opProcs, opSens) = foldl wrapOp ([], []) $
                                        MapSet.toList $ opMap sign
     wrapPred (procsym, axs) (i, predTypes) = let
       procName = mkGenName i
       pProcs = map (\ profile -> (procName,
                        Profile
                           (map (Procparam In) $ predArgs profile)
                           (Just uBoolean))) predTypes
       predTypeSens (PredType w) = let
          xtokens = map (\ (_, ii) -> genNumVar "x" ii) $
                    number w
          xvars = map (
                  \ (si, ii) ->
                  Qual_var (genNumVar "x" ii )
                  si nullRange ) $
                   number w
          ytokens = map (\ (_, ii) -> genNumVar "y" ii) $
                    number w
          btokens = map (\ (_, ii) -> genNumVar "b" ii) $
                    number w
          btoken = genToken "b"
          r1 = genToken "r1"
          r2 = genToken "r2"
          rvar1 = Qual_var (genToken "r1")
                  uBoolean nullRange
          rvar2 = Qual_var (genToken "r2")
                  uBoolean nullRange
          congrP = [makeNamed "" $ Quantification Universal
              (Var_decl (btoken : r1 : r2 : btokens) uBoolean nullRange
               : map (\ ((t1, t2), si) -> Var_decl [t1, t2] si nullRange)
                 (zip (zip xtokens ytokens) w))
               (mkImpl
                  (conjunct
                   (concatMap (\ (si, ii) -> let
                     xv = Qual_var (genNumVar "x" ii)
                           si nullRange
                     yv = Qual_var (genNumVar "y" ii)
                           si nullRange
                     bi1 = Qual_var (genNumVar "b" ii)
                            uBoolean nullRange
                                          in
                     [ExtFORMULA $ Ranged ( Dlformula Diamond
                          (Ranged
                                (Call
                                 (Predication
                                   (Qual_pred_name
                                    (gnRestrName si)
                                    (Pred_type [si] nullRange) nullRange)
                                   [xv] nullRange))
                               nullRange)
                          trueForm ) nullRange ,
                       ExtFORMULA $ Ranged ( Dlformula Diamond
                              (Ranged
                                (Call
                                 (Predication
                                   (Qual_pred_name
                                    (gnRestrName si)
                                    (Pred_type [si] nullRange) nullRange)
                                   [yv] nullRange))
                               nullRange)
                          trueForm ) nullRange ,
                       ExtFORMULA $ mkRanged $ Dlformula Diamond
                              (Ranged
                                (Assign (genNumVar "b" ii)
                            (Application
                             (Qual_op_name
                               (gnEqName si)
                               (Op_type Partial [si, si] uBoolean nullRange)
                              nullRange)
                             [xv, yv] nullRange))
                               nullRange)
                              (mkStEq
                                  bi1 aTrue)
                     ] ) $
                    number w )
                   ) -- hypothesis
                  (ExtFORMULA $ Ranged (
                     Dlformula Diamond
                      (Ranged (Call (Predication
                                   (Qual_pred_name (mkGenName i)
                                    (Pred_type (w ++ [uBoolean]) nullRange)
                                    nullRange)
                                   (map (
                  \ (si, ii) ->
                  Qual_var (genNumVar "x" ii )
                  si nullRange )
                   (number w) ++ [rvar1]) nullRange)) nullRange)
                      (ExtFORMULA $ Ranged (
                         Dlformula Diamond
                      (Ranged (Call (Predication
                                   (Qual_pred_name (mkGenName i)
                                    (Pred_type (w ++ [uBoolean]) nullRange)
                                     nullRange)
                                   (map (
                  \ (si, ii) ->
                  Qual_var (genNumVar "y" ii )
                  si nullRange )
                   (number w) ++ [rvar2]) nullRange)) nullRange)
                       (mkStEq
                                  rvar1
                                  rvar2
                          )
                        ) nullRange)
                   ) nullRange) -- conclusion
                  )
               nullRange
              ]
          termP = [ makeNamed "" $ Quantification Universal
                                     (map
                                             (\ (t1, si) ->
                                              Var_decl [t1] si
                                              nullRange)
                                              (zip xtokens w)
                                      ++ [Var_decl [r1]
                                              uBoolean nullRange])
                      (mkImpl
                         (conjunct
                          (concatMap (\ (si, ii) -> let
                      xv = Qual_var (genNumVar "x" ii)
                            si nullRange
                                           in
                      [ExtFORMULA $ Ranged ( Dlformula Diamond
                           (Ranged
                                 (Call
                                  (Predication
                                    (Qual_pred_name
                                     (gnRestrName si)
                                    (Pred_type [si] nullRange) nullRange)
                                    [xv] nullRange))
                                nullRange)
                           trueForm ) nullRange
                      ] ) $
                     number w )
                          )
                         (ExtFORMULA $ Ranged
                        (
                        Dlformula Diamond
                        (Ranged
                          (Call (Predication (Qual_pred_name (mkGenName i)
                                    (Pred_type (w ++ [uBoolean]) nullRange)
                                     nullRange)
                                 (xvars ++ [rvar1])
                           nullRange))
                         nullRange)
                        trueForm
                        ) nullRange)
                        )
                      nullRange
                    ]
                                   in congrP ++ termP
       pSens = concatMap predTypeSens predTypes
                                                in
      (procsym ++ pProcs, axs ++ pSens)
     (predProcs, predSens) = foldl wrapPred ([], []) $
                                        MapSet.toList $ predMap sign
     procs = Procs $ Map.fromList (sortProcs ++ opProcs ++ predProcs)
     newPreds = procsToPredMap procs
     newOps = procsToOpMap procs
 in (sign { opMap = newOps,
           predMap = newPreds,
           extendedInfo = procs,
           sentences = [] }, sortSens ++ opSens ++ predSens)

mapNamedSen :: Named CASLFORMULA -> Named Sentence
mapNamedSen n_sen = let
 sen = sentence n_sen
 trans = mapCASLSen sen
                    in
 n_sen {sentence = trans}

mapMor :: CASLMor -> VSEMor
mapMor m = let
  (om, pm) = vseMorExt m
  in m
  { msource = fst $ mapSig $ msource m
  , mtarget = fst $ mapSig $ mtarget m
  , op_map = om
  , pred_map = pm
  , extended_map = emptyMorExt
  }

mapCASLSen :: CASLFORMULA -> Sentence
mapCASLSen f = let
 (sen, (_i, vars)) = runState (mapCASLSenAux f) (0, Set.empty)
               in
 case f of
  Sort_gen_ax _ _ -> sen
  _ -> addQuantifiers vars sen

addQuantifiers :: VarSet -> Sentence -> Sentence
addQuantifiers vars sen =
 Quantification Universal
  (map (\ (v, s) -> Var_decl [v] s nullRange) $ Set.toList vars) sen nullRange

mapCASLSenAux :: CASLFORMULA -> State (Int, VarSet) Sentence
mapCASLSenAux f = case f of
  Sort_gen_ax constrs isFree -> do
   let
    (genSorts, _, _ ) = recover_Sort_gen_ax constrs
    toProcs (Op_name _, _) = error "must be qual names"
    toProcs (Qual_op_name op (Op_type _fkind args res _range) _, l) =
           ( Qual_op_name (mkGenName op)
                           (Op_type Partial args res nullRange) nullRange,
             l)
    opsToProcs (Constraint nSort syms oSort) =
                Constraint nSort (map toProcs syms) oSort
   return $ ExtFORMULA $ Ranged
             (RestrictedConstraint
                (map opsToProcs constrs)
                (Map.fromList $ map (\ s -> (s, gnRestrName s)) genSorts)
              isFree)
            nullRange
  Atom b _ps -> return $ boolForm b
  Equation t1 Strong t2 _ps -> do
     let sort1 = sortOfTerm t1
     n1 <- freshIndex sort1 -- (typeof t1)
     prg1 <- mapCASLTerm n1 t1
     n2 <- freshIndex sort1 -- (typeof t2)
     prg2 <- mapCASLTerm n2 t2
     n <- freshIndex uBoolean
     return $ ExtFORMULA $ Ranged
      (Dlformula Diamond
       (Ranged
           (Seq (Ranged (Seq prg1 prg2) nullRange)
                 (Ranged
                 (Assign
                    (genNumVar "x" n)
                    (Application
                       (Qual_op_name
                         (gnEqName sort1)
                         (Op_type Partial [sort1, sort1] uBoolean nullRange)
                        nullRange)
                       [Qual_var (genNumVar "x" n1) sort1 nullRange,
                        Qual_var (genNumVar "x" n2) sort1 nullRange]
                       nullRange
                    )
                 ) nullRange)
           )
        nullRange)
       (mkStEq (Qual_var (genNumVar "x" n) uBoolean nullRange)
                        aTrue)
      )
      nullRange
     {- here i have to return smth like
     --      <: xn1 := prg1;
     --         xn2 := prg2;
     --         xn := gn_eq_s(xn1,xn2) :> xn = True  " -}
  Predication pn as _qs -> do
     indexes <- mapM (freshIndex . sortOfTerm) as
     prgs <- mapM (\ (ti, i) -> mapCASLTerm i ti) $ zip as indexes
     let xvars = map (\ (ti, i) ->
                     Qual_var (genNumVar "x" i)
                              (sortOfTerm ti) nullRange ) $ zip as indexes
     n <- freshIndex uBoolean
     let asgn = if not $ null prgs then
                       foldr1 (\ p1 p2 -> Ranged (Seq p1 p2) nullRange) prgs
                       else Ranged Skip nullRange
     case pn of
      Pred_name _ -> fail "must be qualified"
      Qual_pred_name pname (Pred_type ptype _) _ -> return $ ExtFORMULA $ Ranged
       (Dlformula Diamond
        (Ranged
          (Seq
             asgn
             (Ranged (Assign (genNumVar "x" n)
                       (Application
                         (Qual_op_name
                          (mkGenName pname)
                          (Op_type Partial ptype uBoolean nullRange) nullRange)
                          xvars nullRange))
              nullRange))
         nullRange)
        (mkStEq
          (Qual_var (genNumVar "x" n) uBoolean nullRange)
                        aTrue))
       nullRange
     {- <: xi := prgi;
           x:= gn_p(x1,..,xn):> x = True -}
  Junction j fs _r -> do
   mapFs <- mapM mapCASLSenAux fs
   return $ Junction j mapFs nullRange
  Relation f1 c f2 _r -> do
   trf1 <- mapCASLSenAux f1
   trf2 <- mapCASLSenAux f2
   return $ Relation trf1 c trf2 nullRange
  Negation f1 _r -> do
   trf <- mapCASLSenAux f1
   return $ mkNeg trf
  Quantification q vars sen _ ->
   case q of
    Universal -> do
     trSen <- mapCASLSenAux sen
     let h = map (\ (Var_decl varS s _) -> let
           restrs = map (\ v -> ExtFORMULA $ Ranged (
                                  Dlformula Diamond
                                  (Ranged
                                    (Call
                                      (Predication
                                         (Qual_pred_name
                                            (gnRestrName s)
                                            (Pred_type [s] nullRange)
                                            nullRange
                                         )
                                         [Qual_var v s nullRange]
                                         nullRange
                                      )
                                    )
                                   nullRange)
                                  trueForm) nullRange)
                 varS
                                         in
           conjunct restrs)
             vars
     let sen' = mkImpl
                 (foldr1 (\ sen1 sen2 -> conjunct [sen1, sen2]) h)
                 trSen
     return $ Quantification q vars sen' nullRange
    Existential -> do
     trSen <- mapCASLSenAux sen
     let h = map (\ (Var_decl varS s _) -> let
           restrs = map (\ v -> ExtFORMULA $ Ranged (
                                  Dlformula Diamond
                                  (Ranged
                                    (Call
                                      (Predication
                                         (Qual_pred_name
                                            (gnRestrName s)
                                            (Pred_type [s] nullRange)
                                            nullRange
                                         )
                                         [Qual_var v s nullRange]
                                         nullRange
                                      )
                                    )
                                   nullRange)
                                  trueForm) nullRange)
                 varS
                                         in
           conjunct restrs)
             vars
     let sen' = conjunct
                 [foldr1 (\ sen1 sen2 -> conjunct [sen1, sen2]) h,
                 trSen]
     return $ Quantification q vars sen' nullRange
    Unique_existential -> fail "nyi Unique_existential"
  _ -> fail "Comorphisms.CASL2VSERefine.mapCASLSenAux"


mapCASLTerm :: Int -> TERM () -> State (Int, VarSet) Program
mapCASLTerm n t = case t of
  Qual_var v s _ps -> return $
      Ranged (Assign (genNumVar "x" n)
               (Qual_var v s nullRange)) nullRange
  Application opsym as _qs -> do
   indexes <- mapM (freshIndex . sortOfTerm) as
   let xvars = map (\ (ti, i) ->
                     Qual_var (genNumVar "x" i)
                              (sortOfTerm ti) nullRange ) $ zip as indexes
   prgs <- mapM (\ (ti, i) -> mapCASLTerm i ti) $ zip as indexes
   let asgn = if not $ null prgs then
                       foldr1 (\ p1 p2 -> Ranged (Seq p1 p2) nullRange) prgs
                       else Ranged Skip nullRange
   case opsym of
    Op_name _ -> fail "must be qualified"
    Qual_op_name oName (Op_type _ args res _) _ ->
      case args of
       [] -> return $ Ranged (Assign (genNumVar "x" n)
                       (Application
                        (Qual_op_name
                         (mkGenName oName)
                         (Op_type Partial args res nullRange)
                         nullRange
                        )
                       xvars nullRange))
                       nullRange
       _ -> return $ Ranged
               (Seq
                asgn
                (Ranged (Assign (genNumVar "x" n)
                       (Application
                        (Qual_op_name
                         (mkGenName oName)
                         (Op_type Partial args res nullRange)
                         nullRange
                        )
                       xvars nullRange))
                  nullRange))
                nullRange
  _ -> fail "nyi term"

freshIndex :: SORT -> State (Int, VarSet) Int
freshIndex ss = do
  (i, s) <- get
  let v = genNumVar "x" i
  put (i + 1, Set.insert (v, ss) s)
  return i