content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/CASL2HasCASL.hs
  Description :  embedding CASL into HasCASL
  Copyright   :  (c) Till Mossakowski, Christian Maeder and Uni Bremen 2003-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Logic)
  
  The embedding comorphism from CASL to HasCASL.
  -}
  
  module Comorphisms.CASL2HasCASL where
  
  import Logic.Logic
  import Logic.Comorphism
  
  import Common.AS_Annotation
  import Common.Id
  import Common.ProofTree
  import Common.DocUtils
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  -- CASL
  import CASL.Logic_CASL
  import CASL.Sublogic as CasSub
  import CASL.ToDoc
  import CASL.Fold
  import qualified CASL.AS_Basic_CASL as Cas
  import qualified CASL.Sign as CasS
  import qualified CASL.Morphism as CasM
  
  import HasCASL.Logic_HasCASL
  import HasCASL.As
  import HasCASL.AsUtils
  import HasCASL.Le
  import HasCASL.Builtin
  import HasCASL.Sublogic as HasSub
  import HasCASL.FoldTerm as HasFold
  
  -- | The identity of the comorphism
  data CASL2HasCASL = CASL2HasCASL deriving (Show)
  
  instance Language CASL2HasCASL -- default definition is okay
  
  instance Comorphism CASL2HasCASL
                 CASL CASL_Sublogics
                 CASLBasicSpec Cas.CASLFORMULA Cas.SYMB_ITEMS
                 Cas.SYMB_MAP_ITEMS
                 CasS.CASLSign
                 CasM.CASLMor
                 CasS.Symbol CasM.RawSymbol ProofTree
                 HasCASL Sublogic
                 BasicSpec Sentence SymbItems SymbMapItems
                 Env Morphism Symbol RawSymbol () where
      sourceLogic CASL2HasCASL = CASL
      sourceSublogic CASL2HasCASL = CasSub.top
      targetLogic CASL2HasCASL = HasCASL
      mapSublogic CASL2HasCASL sl = Just $ sublogicUp $
          (if has_cons sl then sublogic_max need_hol else id)
          caslLogic
          { HasSub.has_sub = CasSub.has_sub sl
          , HasSub.has_part = CasSub.has_part sl
          , HasSub.has_eq = CasSub.has_eq sl
          , HasSub.has_pred = CasSub.has_pred sl
          , HasSub.which_logic = case CasSub.which_logic sl of
               CasSub.Atomic -> HasSub.Atomic
               CasSub.Horn -> HasSub.Horn
               CasSub.GHorn -> HasSub.GHorn
               CasSub.Prenex -> HasSub.FOL -- at least for now
               CasSub.FOL -> HasSub.FOL
               CasSub.SOL -> HasSub.HOL
          }
      map_morphism CASL2HasCASL = return . mapMor
      map_sentence CASL2HasCASL _ = return . toSentence
      map_symbol CASL2HasCASL _ = Set.singleton . mapSym
      map_theory CASL2HasCASL = return . mapTheory
      has_model_expansion CASL2HasCASL = True
      is_weakly_amalgamable CASL2HasCASL = True
      isInclusionComorphism CASL2HasCASL = True
  
  fromOPTYPE :: Cas.OP_TYPE -> Type
  fromOPTYPE (Cas.Op_type ok args res ps) = let
    (total, arr) = case ok of
      Cas.Total -> (True, FunArr)
      Cas.Partial -> (False, PFunArr)
    resTy = toType res
    in if null args then if total then resTy else mkLazyType resTy
    else mkFunArrType (mkProductTypeWithRange (map toType args) ps) arr resTy
  
  fromOpType :: CasS.OpType -> Type
  fromOpType = fromOPTYPE . CasS.toOP_TYPE
  
  fromPREDTYPE :: Cas.PRED_TYPE -> Type
  fromPREDTYPE (Cas.Pred_type args ps) =
     if null args then mkLazyType $ unitTypeWithRange ps
     else predType ps $ mkProductTypeWithRange (map toType args) ps
  
  fromPredType :: CasS.PredType -> Type
  fromPredType = fromPREDTYPE . CasS.toPRED_TYPE
  
  mapTheory :: (CasS.TermExtension f, FormExtension f) =>
    (CasS.Sign f e, [Named (Cas.FORMULA f)]) -> (Env, [Named Sentence])
  mapTheory (sig, sents) =
    (mapSig (CasS.getConstructors sents) sig, map (mapNamed toSentence) sents)
  
  mapSig :: Set.Set (Id, CasS.OpType) -> CasS.Sign f e -> Env
  mapSig = mapSigAux trId fromOpType fromPredType
  
  -- | sort names or not translated
  mapSigAux :: (Id -> Id) -> (CasS.OpType -> Type) -> (CasS.PredType -> Type)
    -> Set.Set (Id, CasS.OpType) -> CasS.Sign f e -> Env
  mapSigAux trI trO trP constr sign =
      let f1 = map ( \ (i, ty) ->
                     (trI i, trO ty,
                              if Set.member (i, CasS.mkPartial ty)
                                 constr then ConstructData $ CasS.opRes ty
                                 else NoOpDefn Op))
               $ CasS.mapSetToList $ CasS.opMap sign
          f2 = map ( \ (i, ty) -> let pTy = trP ty in
                     (trI i, pTy, NoOpDefn
                     $ if isPredType pTy then Pred else Fun))
               $ CasS.mapSetToList $ CasS.predMap sign
          insF (i, ty, defn) m =
              let os = Map.findWithDefault Set.empty i m
              in Map.insert i (Set.insert
                               (OpInfo (simpleTypeScheme ty) Set.empty defn) os) m
       in initialEnv
       { classMap = Map.empty,
         typeMap = Map.fromList $ map
                   ( \ s -> (s, starTypeInfo
                             { superTypes = Set.delete s $
                                            CasS.supersortsOf s sign
                             })) $ Set.toList $ CasS.sortSet sign,
         assumps = foldr insF Map.empty (f1 ++ f2)}
  
  mapMor :: CasM.Morphism f e m -> Morphism
  mapMor m = let tm = CasM.sort_map m
                 f1 = map ( \ ((i, ot), (j, t)) ->
                            ((trId i, simpleTypeScheme $ fromOpType ot),
                             (trId j, simpleTypeScheme $ mapType tm
                                   $ fromOpType ot { CasS.opKind = t })))
                      $ Map.toList $ CasM.op_map m
                 f2 = map ( \ ((i, pt), j) ->
                            let ty = fromPredType pt
                            in ( (trId i, simpleTypeScheme ty)
                               , (trId j, simpleTypeScheme $ mapType tm ty)))
                      $ Map.toList $ CasM.pred_map m
              in (mkMorphism (mapSig Set.empty $ CasM.msource m)
                                 (mapSig Set.empty $ CasM.mtarget m))
             { typeIdMap = tm , funMap = Map.fromList $ f2 ++ f1 }
  
  mapSym :: CasS.Symbol -> Symbol
  mapSym = mapSymAux trId fromOpType fromPredType
  
  mapSymAux :: (Id -> Id) -> (CasS.OpType -> Type)
    -> (CasS.PredType -> Type) -> CasS.Symbol -> Symbol
  mapSymAux trI trO trP s = let
    n = CasS.symName s
    i = trI n
    in case CasS.symbType s of
      CasS.OpAsItemType ot -> idToOpSymbol i . simpleTypeScheme $ trO ot
      CasS.PredAsItemType pt -> idToOpSymbol i . simpleTypeScheme $ trP pt
      CasS.SortAsItemType -> idToTypeSymbol n rStar
      CasS.SubsortAsItemType _ -> idToTypeSymbol n rStar
  
  toQuant :: Cas.QUANTIFIER -> Quantifier
  toQuant Cas.Universal = Universal
  toQuant Cas.Existential = Existential
  toQuant Cas.Unique_existential = Unique
  
  toVarDecl :: Cas.VAR_DECL -> [GenVarDecl]
  toVarDecl (Cas.Var_decl vs s ps) =
             map ( \ i -> GenVarDecl $
                   VarDecl (simpleIdToId i) (toType s) Other ps) vs
  
  toSentence :: (CasS.TermExtension f, FormExtension f)
    => Cas.FORMULA f -> Sentence
  toSentence f = case f of
     Cas.Sort_gen_ax cs b -> let
         (sorts, ops, smap) = Cas.recover_Sort_gen_ax cs
         genKind = if b then Free else Generated
         mapPart :: Cas.OpKind -> Partiality
         mapPart cp = case cp of
                  Cas.Total -> HasCASL.As.Total
                  Cas.Partial -> HasCASL.As.Partial
         in DatatypeSen $ map ( \ s ->
            DataEntry (Map.fromList smap) s genKind [] rStar
            $ Set.fromList $ map ( \ (i, t) ->
              let args = map toType $ CasS.opArgs t in
              Construct (if isInjName i then Nothing else Just i)
                (if null args then [] else [mkProductType args])
                (mapPart $ CasS.opKind t)
                $ if null args then [] else
                [map (\ a -> Select Nothing a HasCASL.As.Total) args])
            $ filter ( \ (_, t) -> CasS.opRes t == s)
                  $ map ( \ o -> case o of
                          Cas.Qual_op_name i t _ -> (trId i, CasS.toOpType t)
                          _ -> error "CASL2HasCASL.toSentence") ops) sorts
     _ -> Formula $ toTerm f
  
  toTerm :: (CasS.TermExtension f, FormExtension f) => Cas.FORMULA f -> Term
  toTerm f = foldFormula (transRecord $ showDoc f "") f
  
  transRecord :: CasS.TermExtension f => String -> Record f Term Term
  transRecord str = let err = error $ "CASL2HasCASL.unexpected formula: " ++ str
    in (constRecord err err err)
    { foldQuantification = \ _ q -> QuantifiedTerm (toQuant q)
          . concatMap toVarDecl
    , foldJunction = \ _ j fs ps -> let
         (n, op) = case j of
            Cas.Con -> (trueId, andId)
            Cas.Dis -> (falseId, orId)
         in case fs of
          [] -> unitTerm n ps
          _ -> toBinJunctor op fs ps
    , foldRelation = \ _ f1 c f2 ps -> case c of
         Cas.Implication -> mkLogTerm implId ps f1 f2
         Cas.RevImpl -> mkLogTerm infixIf ps f2 f1
         Cas.Equivalence -> mkLogTerm eqvId ps f1 f2
    , foldNegation = \ _ frm ps -> mkTerm notId notType [] ps frm
    , foldAtom = \ _ b -> unitTerm $ if b then trueId else falseId
    , foldEquation = \ o t1 e t2 ps ->
          let Cas.Equation c1 _ _ _ = o in
          mkEqTerm (if e == Cas.Existl then exEq else eqId)
                       (typeOfTerm c1) ps t1 t2
    , foldPredication = \ _ qpn args qs ->
          let Cas.Qual_pred_name ui pty@(Cas.Pred_type ts _) ps = qpn
              i = trId ui
              sc = simpleTypeScheme $ fromPREDTYPE pty
              p = QualOp Pred (PolyId i [] ps) sc [] Infer ps
              in if null args then p else TypedTerm
                (ApplTerm p (mkTupleTerm (zipWith
                 (\ tr ty -> TypedTerm tr Inferred (toType ty) ps)
                  args ts) qs) qs)
                Inferred unitType ps
    , foldDefinedness = \ o t ps ->
          let Cas.Definedness c _ = o in
          mkTerm defId defType [typeOfTerm c] ps t
    , foldMembership = \ _ t -> TypedTerm t InType . toType
    , foldQuantOp = \ _ uo ty frm -> let o = trId uo in
           QuantifiedTerm Universal
           [GenVarDecl $ VarDecl o (fromOPTYPE ty) Other nullRange]
           (qualName2var o frm) nullRange
    , foldQuantPred = \ _ up ty frm -> let p = trId up in
           QuantifiedTerm Universal
           [GenVarDecl $ VarDecl p (fromPREDTYPE ty) Other nullRange]
           (qualName2var p frm) nullRange
    , foldQual_var = \ _ v ty ->
          QualVar . VarDecl (simpleIdToId v) (toType ty) Other
    , foldApplication = \ _ qon args qs ->
          let Cas.Qual_op_name ui ot ps = qon
              i = trId ui
              sc = simpleTypeScheme $ fromOPTYPE ot
              o = QualOp Op (PolyId i [] ps) sc [] Infer ps
              at = CasS.toOpType ot
          in if null args then o else TypedTerm
             (ApplTerm o (mkTupleTerm (zipWith
                 (\ tr ty -> TypedTerm tr Inferred (toType ty) ps)
                  args $ CasS.opArgs at) qs) qs)
             Inferred (toType $ CasS.opRes at) ps
    , foldSorted_term = \ _ trm -> TypedTerm trm OfType . toType
    , foldCast = \ _ trm -> TypedTerm trm AsType . toType
    , foldConditional = \ o t1 f t2 ps ->
          let Cas.Conditional c1 _ _ _ = o in
          mkTerm whenElse whenType [typeOfTerm c1] ps
            $ TupleTerm [t1, f, t2] ps
    , foldSort_gen_ax = \ _ cs _ ->
        error $ "unexpected sort generation constraint: "
        ++ unlines (map (`showDoc` "") $ recoverType cs)
        ++ "in: " ++ str
    }
  
  typeOfTerm :: CasS.TermExtension f => Cas.TERM f -> Type
  typeOfTerm = toType . CasS.sortOfTerm
  
  -- | replace qualified names by variables in second order formulas
  qualName2var :: Id -> Term -> Term
  qualName2var i = HasFold.foldTerm mapRec
    { foldQualOp = \ t _ (PolyId j _ _) (TypeScheme _ ty _) _ _ ps ->
        if i == j then QualVar $ VarDecl i ty Other ps else t }
  
  -- | the invisible identifier is reserved for application
  trId :: Id -> Id
  trId i@(Id ts cs ps) = if null cs && all isPlace ts then
    Id [genNumVar "empty" $ length ts] cs ps else i
  