{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  $Header$
Description :  Coding a description language into CASL
Copyright   :  (c)  Stef Joosten, Christian Maeder DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

The translating comorphism from Adl to CASL.
-}

module Comorphisms.Adl2CASL
    ( Adl2CASL (..)
    ) where

import Logic.Logic
import Logic.Comorphism

-- Adl
import Adl.Logic_Adl as A
import Adl.As
import Adl.Sign as A

-- CASL
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sublogic
import CASL.Sign as C
import CASL.Morphism as C
import CASL.Fold
import CASL.Overload

import Common.AS_Annotation
import Common.DefaultMorphism
import Common.DocUtils
import Common.Id
import Common.ProofTree
import Common.Result
import Common.Token
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet
import Common.Lib.State

import qualified Data.Set as Set

-- | lid of the morphism
data Adl2CASL = Adl2CASL deriving Show

instance Language Adl2CASL -- default is ok

instance Comorphism Adl2CASL
    Adl
    ()
    Context
    Sen
    ()
    ()
    A.Sign
    A.Morphism
    A.Symbol
    A.RawSymbol
    ProofTree
    CASL
    CASL_Sublogics
    CASLBasicSpec
    CASLFORMULA
    SYMB_ITEMS
    SYMB_MAP_ITEMS
    CASLSign
    CASLMor
    C.Symbol
    C.RawSymbol
    ProofTree
    where
      sourceLogic Adl2CASL = Adl
      sourceSublogic Adl2CASL = ()
      targetLogic Adl2CASL = CASL
      mapSublogic Adl2CASL _ = Just $ caslTop
        { has_part = False
        , sub_features = LocFilSub
        , cons_features = NoSortGen }
      map_theory Adl2CASL = mapTheory
      map_sentence Adl2CASL s = return . mapSen (mapSign s)
      map_morphism Adl2CASL = mapMor
      map_symbol Adl2CASL _ = Set.singleton . mapSym
      is_model_transportable Adl2CASL = True
      has_model_expansion Adl2CASL = True
      is_weakly_amalgamable Adl2CASL = True
      isInclusionComorphism Adl2CASL = True

mapTheory :: (A.Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory (s, ns) = let cs = mapSign s in
  return (cs, map (mapNamed $ mapSen cs) ns)

relTypeToPred :: RelType -> PredType
relTypeToPred (RelType c1 c2) = PredType [conceptToId c1, conceptToId c2]

mapSign :: A.Sign -> CASLSign
mapSign s = (C.emptySign ())
  { sortRel = Rel.transClosure $ Rel.union
       (Rel.fromKeysSet $ Set.fold (\ sy -> case sy of
                 Con (C i) -> Set.insert $ simpleIdToId i
                 _ -> id) Set.empty $ A.symOf s)
       $ Rel.map conceptToId $ isas s
  , predMap = MapSet.fromList
      . map (\ (i, l) -> (transRelId $ idToSimpleId i, l))
      . MapSet.toList . MapSet.map relTypeToPred . MapSet.fromMap $ rels s
  }

transRelId :: Token -> Id
transRelId t@(Token s p) = simpleIdToId $
   if elem s casl_reserved_fwords then Token ("P_" ++ s) p else t

mapSen :: CASLSign -> Sen -> CASLFORMULA
mapSen sig s = case s of
  DeclProp r p -> getRelProp sig r p
  Assertion _ r ->
    let ((v1, s1), (v2, s2), f) = evalState (transRule sig r) 1 in
    mkForall [mkVarDecl v1 s1, mkVarDecl v2 s2] f

-- | Translation of morphisms
mapMor :: A.Morphism -> Result CASLMor
mapMor mor = return $ embedMorphism ()
    (mapSign $ domOfDefaultMorphism mor) $ mapSign $ codOfDefaultMorphism mor

mapSym :: A.Symbol -> C.Symbol
mapSym s = case s of
  Con c -> idToSortSymbol $ conceptToId c
  Rel (Sgn n t) -> idToPredSymbol (transRelId n) $ relTypeToPred t

next :: State Int Int
next = do
  i <- get
  put $ i + 1
  return i

getRelPred :: CASLSign -> Relation -> PRED_SYMB
getRelPred sig m@(Sgn t (RelType c1 c2)) = let
  ty1 = conceptToId c1
  ty2 = conceptToId c2
  i = transRelId t
  cs = filter (\ pt -> case predArgs pt of
                  [fr, to] -> leqSort sig ty1 fr && leqSort sig ty2 to
                  _ -> False)
               $ Set.toList $ MapSet.lookup i $ predMap sig
  in case cs of
       ty : _ ->
           Qual_pred_name i (toPRED_TYPE ty) $ tokPos t
       _ -> error $ "getRelPred " ++ showDoc m ""

getRelProp :: CASLSign -> Relation -> RangedProp -> CASLFORMULA
getRelProp sig r p =
  let qp@(Qual_pred_name _ (Pred_type [fr, to] _) _) = getRelPred sig r
      q = propRange p
      q1 = Var_decl [mkSimpleId "a"] fr q
      q2 = Var_decl [mkSimpleId "b"] to q
      q3 = Var_decl [mkSimpleId "c"] fr q
      t1 = toQualVar q1
      t2 = toQualVar q2
      t3 = toQualVar q3
      pAppl = Predication qp [t1, t2] q
      eqs = fr == to
  in case propProp p of
       Uni -> mkForallRange [q1, q2, q3]
            (Implication
             (Conjunction
              [pAppl, Predication qp [t3, t2] q] q)
             (Strong_equation t1 t3 q)
             True q) q
       Tot -> mkForallRange [q1] (Quantification Existential [q2] pAppl q) q
       Sur -> mkForallRange [q2] (Quantification Existential [q1] pAppl q) q
       Inj -> let
         q4 = Var_decl [mkSimpleId "c"] to q
         t4 = toQualVar q4
         in mkForallRange [q1, q2, q4]
            (Implication
             (Conjunction
              [pAppl, Predication qp [t1, t4] q] q)
             (Strong_equation t2 t4 q)
             True q) q
       Sym | eqs -> mkForallRange [q1, q2]
         (Equivalence pAppl (Predication qp [t2, t1] q) q) q
       Asy | eqs -> mkForallRange [q1, q2]
         (Implication pAppl (Negation (Predication qp [t2, t1] q) q) True q) q
       Trn | eqs -> mkForallRange [q1, q2, q3]
          (Implication
           (Conjunction [pAppl, Predication qp [t2, t3] q] q)
             (Predication qp [t1, t3] q)
             True q) q
       Rfx | eqs -> mkForallRange [q1] (Predication qp [t1, t1] q) q
       pr -> error $ "getRelProp " ++ showDoc pr ""

transRule :: CASLSign -> Rule
          -> State Int ((VAR, SORT), (VAR, SORT), CASLFORMULA)
transRule sig rule =
  let myMin v@(ta, sa) (_, sb) =
               if leqSort sig sa sb then v else
               if leqSort sig sb sa then (ta, sb) else
                   error $ "transRule.myMin " ++ showDoc (sa, sb) "\n "
                   ++ showDoc rule ""
      myVarDecl = uncurry mkVarDecl
  in case rule of
  Tm m@(Sgn (Token s p) (RelType c1 c2)) -> do
      i <- next
      j <- next
      let v1 = mkNumVar "a" i
          v2 = mkNumVar "b" j
          isI = s == "I"
          ty1' = conceptToId c1
          ty2' = conceptToId c2
          ty1 = if isI && leqSort sig ty2 ty1 then ty2' else ty1'
          ty2 = if isI && leqSort sig ty1 ty2 then ty1' else ty2'
          q1 = Qual_var v1 ty1 p
          q2 = Qual_var v2 ty2 p
      return ((v1, ty1), (v2, ty2),
        if s == "V" then True_atom p else
        if isI then
            if ty1 == ty2 then Strong_equation q1 q2 p else
                error $ "transRule.I " ++ showDoc rule ""
        else
          let qp@(Qual_pred_name _ (Pred_type [fr, to] _) _) = getRelPred sig m
          in Predication qp
            [ if ty1 == fr then q1 else Sorted_term q1 fr p
            , if ty2 == to then q2 else Sorted_term q2 to p] p)
  UnExp o e -> do
    (v1, v2@(t2, _), f) <- transRule sig e
    case o of
      Co -> return (v2, v1, f)
      Cp -> return (v1, v2, negateForm f nullRange)
      _ -> do
        k <- next
        let v@(_, s) = myMin v1 v2
            w = (t2, s)
            nf = renameVar sig v1 v $ renameVar sig v2 w f
            z = (mkNumVar "c" k, s)
            cf = mkExist [myVarDecl z]
                 $ conjunct [renameVar sig v z nf, renameVar sig w z nf]
        -- this is (and always will be) incomplete wrt to compositions
        return (v, w, disjunct
           $ [ mkStEq (toQualVar $ myVarDecl v) $ toQualVar $ myVarDecl w
             | o == K0] ++ [nf, cf])
  MulExp o es -> case es of
    [] -> error "transRule2"
    r : t -> if null t then transRule sig r else do
       (v1, v2, f1) <- transRule sig r
       (v3, v4, f2) <- transRule sig $ MulExp o t
       if elem o [Fc, Fd] then return (v1, v4,
         let v23 = myMin v2 v3
             f3 = renameVar sig v2 v23 f1
             f4 = renameVar sig v3 v23 f2
             vs = [myVarDecl v23]
             cs = [f3, f4]
         in if o == Fc then mkExist vs $ conjunct cs
              else mkForall vs $ disjunct cs)
         else do
           let v13 = myMin v1 v3
               v24 = myMin v2 v4
               f3 = renameVar sig v1 v13 $ renameVar sig v2 v24 f1
               f4 = renameVar sig v3 v13 $ renameVar sig v4 v24 f2
           return (v13, v24, case o of
             Fi -> conjunct [f3, f4]
             Fu -> disjunct [f3, f4]
             Ri -> mkImpl f3 f4
             Rr -> Implication f4 f3 False nullRange
             Re -> mkEqv f3 f4
             _ -> error "transRule,MulExp")

renameVarRecord :: CASLSign -> (VAR, SORT) -> (VAR, SORT)
                -> Record () CASLFORMULA (TERM ())
renameVarRecord sig from to = (mapRecord id)
  { foldQual_var = \ _ v ty p ->
      let (nv, nty) = if (v, ty) == from then to else (v, ty)
          qv = Qual_var nv nty p
      in if nty == ty then qv else
         if leqSort sig nty ty then Sorted_term qv ty p else
             error "renameVar"
  }

renameVar :: CASLSign -> (VAR, SORT) -> (VAR, SORT) -> CASLFORMULA
          -> CASLFORMULA
renameVar sig v = foldFormula . renameVarRecord sig v
