content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/Adl2CASL.hs
  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 as A
  import Adl.Sign as A
  
  -- CASL
  import CASL.Logic_CASL
  import CASL.AS_Basic_CASL as C
  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
                   A.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
    A.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 -> A.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 -> A.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]
              (Relation
               (conjunctRange
                [pAppl, Predication qp [t3, t2] q] q)
               Implication (Equation t1 Strong t3 q)
               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]
              (Relation
               (conjunctRange
                [pAppl, Predication qp [t1, t4] q] q)
               Implication (Equation t2 Strong t4 q)
               q) q
         Sym | eqs -> mkForallRange [q1, q2]
           (Relation pAppl Equivalence (Predication qp [t2, t1] q) q) q
         Asy | eqs -> mkForallRange [q1, q2]
           (Relation pAppl Implication
            (Negation (Predication qp [t2, t1] q) q) q) q
         Trn | eqs -> mkForallRange [q1, q2, q3]
            (Relation
             (conjunctRange [pAppl, Predication qp [t2, t3] q] q)
               Implication (Predication qp [t1, t3] q)
               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)
          | leqSort sig sa sb = v
          | leqSort sig sb sa = (ta, sb)
          | otherwise = 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 Atom True p else
          if isI then
              if ty1 == ty2 then Equation q1 Strong 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 -> Relation f4 RevImpl f3 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
  