content: {-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
  {- |
  Module      :  ./CASL/OMDocExport.hs
  Description :  CASL-to-OMDoc conversion
  Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  ewaryst.schulz@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  CASL implementation of the interface functions export_signToOmdoc,
  export_morphismToOmdoc, export_senToOmdoc from class Logic. The actual
  instantiation can be found in module "CASL.Logic_CASL".
  -}
  
  module CASL.OMDocExport
      ( exportSymToOmdoc
      , exportSenToOmdoc
      , exportTheoryToOmdoc
      , caslMetaTheory
      ) where
  
  import OMDoc.DataTypes
  
  import Common.Id
  import Common.Result
  import Common.AS_Annotation
  import qualified Common.Lib.Rel as Rel
  import qualified Control.Monad.Fail as Fail
  
  import Common.DocUtils
  
  import CASL.AS_Basic_CASL
  import CASL.Sign
  import CASL.Fold
  import CASL.Quantification
  import CASL.OMDoc
  
  import qualified Data.Map as Map
  import Data.Maybe
  
  -- --------------------------- TOPLEVEL Interface -----------------------------
  
  type Env = NameMap Symbol
  
  
  exportSymToOmdoc :: Env -> Symbol -> String -> Result TCElement
  exportSymToOmdoc e sym n = toOMConstant e (n, symbType sym)
  
  
  exportSenToOmdoc :: (GetRange f, Pretty f) => Env -> FORMULA f
                   -> Result TCorOMElement
  exportSenToOmdoc e f =
      case f of
          Sort_gen_ax cs b -> return $ Left $ makeADTs e cs
                              (if b then Free else Generated)
          _ -> let err = const $ error "CASL extension not supported."
               in return $ Right $ foldFormula (omdocRec e err) f
  
  -- | We have to export the subsort relation because it's not given in sentences
  exportTheoryToOmdoc :: (Show f, Pretty e) => SigMap Symbol -> Sign f e
                      -> [Named (FORMULA f)] -> Result [TCElement]
  
  exportTheoryToOmdoc sigm sig _ =
      return $ map (subsortToOmdoc $ sigMapSymbs sigm)
        $ Rel.toList $ Rel.reflexive $ sortRel sig
  
  
  -- ------------------------ Sentences --------------------------
  
  subsortToOmdoc :: Env -> (SORT, SORT) -> TCElement
  subsortToOmdoc e (s1, s2) =
      let oms1@(OMS (_, OMName n1 _)) = oms e s1
          oms2@(OMS (_, OMName n2 _)) = oms e s2
      in TCSymbol (nameEncode "ST" [n1, n2])
             (OMA [const_subsortof, oms1, oms2]) Axiom Nothing
  
  
  -- ------------------------ Symbol Interface --------------------------
  
  class AsSymbol a where
      toSymbol :: a -> Symbol
  
  instance AsSymbol SORT where
      toSymbol = idToSortSymbol
  
  instance AsSymbol (Id, OpType) where
      toSymbol = uncurry idToOpSymbol
  
  instance AsSymbol (Id, OP_TYPE) where
      toSymbol (x, y) = toSymbol (x, toOpType y)
  
  instance AsSymbol OP_SYMB where
      toSymbol (Op_name n) = error $ "AsSymbol: Unqualified OP_SYMB: " ++ show n
      toSymbol (Qual_op_name n t _) = toSymbol (n, t)
  
  instance AsSymbol (Id, PredType) where
      toSymbol = uncurry idToPredSymbol
  
  instance AsSymbol (Id, PRED_TYPE) where
      toSymbol (x, y) = toSymbol (x, toPredType y)
  
  instance AsSymbol PRED_SYMB where
      toSymbol (Pred_name n) = error $ "AsSymbol: Unqual. PRED_SYMB: " ++ show n
      toSymbol (Qual_pred_name n t _) = toSymbol (n, t)
  
  -- ------------------------ OMDoc Constant Interface --------------------------
  
  class AsOMConstant a where
      toOMConstant :: Env -> a -> Result TCElement
  
  
  instance AsOMConstant (String, OMElement, SymbolRole) where
      toOMConstant _ (n, omelem, role) = return $ TCSymbol n omelem role Nothing
  
  instance AsOMConstant (String, OpType) where
      toOMConstant e (n, ot) = toOMConstant e (n, makeObjectType e ot, Obj)
  
  instance AsOMConstant (String, PredType) where
      toOMConstant e (n, pt) = toOMConstant e (n, makePredType e pt, Obj)
  
  instance AsOMConstant String where
      toOMConstant e n = toOMConstant e (n, const_sort, Typ)
  
  instance AsOMConstant (String, SymbType) where
      toOMConstant e (n, st) =
          case st of
            SortAsItemType -> toOMConstant e n
            SubsortAsItemType _ -> Fail.fail "AsOMConstant.SubsortAsItemType"
            OpAsItemType ot -> toOMConstant e (n, ot)
            PredAsItemType pt -> toOMConstant e (n, pt)
  
  -- ------------------------ ADT --------------------------
  
  makeADTs :: Env -> [Constraint] -> ADTType -> TCElement
  makeADTs e cs b =
      TCADT $ map (makeADTSortDef e b) cs
  
  makeADTSortDef :: Env -> ADTType -> Constraint -> OmdADT
  makeADTSortDef e b (Constraint s l _) =
      ADTSortDef (omn e s) b $
      map (makeADTConstructor e . fst) l
  
  makeADTConstructor :: Env -> OP_SYMB -> OmdADT
  makeADTConstructor e os@(Qual_op_name n (Op_type _ args _ _) _) =
      if isInjName n then ADTInsort $ omqn e $ head args
      else ADTConstr (omn e os) $ map (makeADTArgument e) args
  
  makeADTConstructor _ (Op_name (Id _ _ r)) =
      sfail "makeADTConstructor: No_qual_op" r
  
  -- TODO: support for selectors
  makeADTArgument :: Env -> SORT -> OmdADT
  makeADTArgument e s = ADTArg (oms e s) Nothing
  
  
  -- ------------------------ UTILS --------------------------
  
  findInEnv :: UniqName -> Env -> Symbol -> UniqName
  findInEnv err m x = fromMaybe (case symbType x of
       OpAsItemType o -> Map.findWithDefault err
          x { symbType = OpAsItemType
              $ (if isTotal o then mkPartial else mkTotal) o } m
       _ -> err) $ Map.lookup x m
  
  sfail :: String -> Range -> a
  sfail s r = error $ show (Diag Error ("unexpected " ++ s) r)
  
  omn :: AsSymbol a => Env -> a -> String
  omn e x = let s = toSymbol x
                err = error $ concat [ "omn: No mapping for ", show s, "\n"
                                     , "--------------------------------\n"
                                     , show e]
            in nameToString $ findInEnv err e s
  
  omqn :: AsSymbol a => Env -> a -> OMQualName
  omqn e x = let s = toSymbol x
                 err = error $ concat [ "omqn: No mapping for ", show s, "\n"
                                      , "--------------------------------\n"
                                      , show e]
             in mkSimpleQualName $ findInEnv err e s
  
  oms :: AsSymbol a => Env -> a -> OMElement
  oms e x = let s = toSymbol x
                err = error $ "oms: No mapping for " ++ show s
            in simpleOMS $ findInEnv err e s
  
  
  -- ------------------------ TYPES --------------------------
  
  -- | Given an operator or predicate signature we construct the according type
  makeType :: Env -> OpKind -> [SORT] -> Maybe SORT -> OMElement
  makeType e _ [] (Just r) = oms e r
  makeType e total domain range =
      if null args then funtypeconstr else OMA $ funtypeconstr : map (oms e) args
          where
            args = domain ++ maybeToList range
            funtypeconstr = case (total, range) of
                              (Total, Nothing) -> const_predtype
                              (Total, _) -> const_funtype
                              _ -> const_partialfuntype
  
  makePredType :: Env -> PredType -> OMElement
  makePredType e (PredType predargs) =
      makeType e Total predargs Nothing
  
  makeObjectType :: Env -> OpType -> OMElement
  makeObjectType e (OpType opkind opargs oprange) =
      makeType e opkind opargs (Just oprange)
  
  -- ------------------------ TERMS --------------------------
  
  appOrConst :: AsSymbol a => Env -> a -> [OMElement] -> OMElement
  appOrConst e o [] = oms e o
  appOrConst e o ts = OMA $ oms e o : ts
  
  -- | The object e1 and its type e2
  makeTyped :: OMElement -- ^ e1
            -> OMElement -- ^ e2
            -> OMElement
  makeTyped e1 e2 = OMATTT e1 $ OMAttr const_type e2
  
  varToOmdoc :: Token -> OMElement
  varToOmdoc v = OMV $ mkSimpleName $ tokStr v
  
  -- | typed vars can only be typed by a single sort (first order)
  varDeclToOMDoc :: Env -> (VAR, SORT) -> OMElement
  varDeclToOMDoc e (v, s) = makeTyped (varToOmdoc v) $ oms e s
  
  omdocRec :: GetRange f => Env -> (f -> OMElement)
           -> Record f OMElement OMElement
  omdocRec e mf = Record
      { foldQuantification = \ _ q vs f _ ->
        let s = case q of
                  Universal -> const_forall
                  Existential -> const_exists
                  Unique_existential -> const_existsunique
            vl = map (varDeclToOMDoc e) $ flatVAR_DECLs vs
        in OMBIND s vl f
      , foldJunction = \ _ j fs _ -> OMA $ case j of
            Con -> const_and
            Dis -> const_or
          : fs
      , foldRelation = \ _ f1 c f2 _ -> OMA $ case c of
            Implication -> const_implies
            RevImpl -> const_implied
            Equivalence -> const_equivalent
          : [f1, f2]
      , foldNegation = \ _ f _ -> OMA [const_not, f]
      , foldAtom = \ _ b _ -> if b then const_true else const_false
      , foldPredication = \ _ p ts _ -> appOrConst e p ts
      , foldDefinedness = \ _ t _ -> OMA [const_def, t]
      , foldEquation = \ _ t1 r t2 _ -> OMA $ case r of
            Existl -> const_eeq
            Strong -> const_eq
          : [t1, t2]
      , foldMembership = \ _ t s _ -> OMA [const_in, t, oms e s]
      , foldMixfix_formula = \ t _ -> sfail "Mixfix_formula" $ getRange t
      , foldQuantOp = \ _ o _ _ -> sfail ("QuantOp " ++ show o) $ getRange o
      , foldQuantPred = \ _ p _ _ -> sfail ("QuantPred " ++ show p) $ getRange p
      , foldSort_gen_ax = \ t _ _ -> sfail
                          "Sort generating axioms should be filtered out before!"
                          $ getRange t
      , foldExtFORMULA = const mf
      , foldQual_var = \ _ v _ _ -> varToOmdoc v
      , foldApplication = \ _ o ts _ -> appOrConst e o ts
      , foldSorted_term = \ _ r s _ -> makeTyped r $ oms e s
      , foldCast = \ _ t s _ -> OMA [const_cast, t, oms e s]
      , foldConditional = \ _ e' f t _ -> OMA [const_if, e', f, t]
      , foldMixfix_qual_pred = \ _ p -> sfail "Mixfix_qual_pred" $ getRange p
      , foldMixfix_term = \ t _ -> sfail "Mixfix_term" $ getRange t
      , foldMixfix_token = \ _ t -> sfail "Mixfix_token" $ tokPos t
      , foldMixfix_sorted_term = \ _ _ r -> sfail "Mixfix_sorted_term" r
      , foldMixfix_cast = \ _ _ r -> sfail "Mixfix_cast" r
      , foldMixfix_parenthesized = \ _ _ r -> sfail "Mixfix_parenthesized" r
      , foldMixfix_bracketed = \ _ _ r -> sfail "Mixfix_bracketed" r
      , foldMixfix_braced = \ _ _ r -> sfail "Mixfix_braced" r
      , foldExtTERM = const mf }
  