OMDocImport.hs

{- |
Module      :  $Header$
Description :  OMDoc-to-CASL 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 omdocToSym, omdocToSen
, addOMadtToTheory, addOmdocToTheory from class Logic. The actual
instantiation can be found in module "CASL.Logic_CASL".
-}

module CASL.OMDocImport
    ( omdocToSym
    , omdocToSen
    , addOMadtToTheory
    , addOmdocToTheory
    ) where

import OMDoc.DataTypes

import Common.Id
import Common.Result
import Common.AS_Annotation
import qualified Common.Lib.Rel as Rel

import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.OMDoc

import Control.Monad

import qualified Data.Map as Map
import Data.List

-- * Environment Interface

type Env = SigMapI Symbol

symbolToSort :: Symbol -> SORT
symbolToSort (Symbol n SortAsItemType) = n
symbolToSort s = error $ "symbolToSort: Nonsort encountered: " ++ show s

symbolToOp :: Symbol -> (Id, OpType)
symbolToOp (Symbol n (OpAsItemType ot)) = (n, ot)
symbolToOp s = error $ "symbolToOp: Nonop encountered: " ++ show s

symbolToPred :: Symbol -> (Id, PredType)
symbolToPred (Symbol n (PredAsItemType pt)) = (n, pt)
symbolToPred s = error $ "symbolToPred: Nonpred encountered: " ++ show s

lookupSymbol :: Env -> OMName -> Symbol
lookupSymbol e omn =
    Map.findWithDefault
           (error $ concat [ "lookupSymbol failed for: "
                           , show omn, "\nmap: ", show $ sigMapISymbs e])
       omn $ sigMapISymbs e

lookupSort :: Env -> OMName -> SORT
lookupSort e = symbolToSort . lookupSymbol e

lookupSortOMS :: String -> Env -> OMElement -> SORT
lookupSortOMS msg = lookupOMS lookupSort $ msg ++ "(SORT)"

lookupPred :: Env -> OMName -> (Id, PredType)
lookupPred e = symbolToPred . lookupSymbol e

lookupPredOMS :: String -> Env -> OMElement -> (Id, PredType)
lookupPredOMS msg = lookupOMS lookupPred $ msg ++ "(PRED)"

lookupOp :: Env -> OMName -> (Id, OpType)
lookupOp e = symbolToOp . lookupSymbol e

lookupOpOMS :: String -> Env -> OMElement -> (Id, OpType)
lookupOpOMS msg = lookupOMS lookupOp $ msg ++ "(Op)"

lookupOMS :: (Env -> OMName -> a) -> String -> Env -> OMElement -> a
lookupOMS f msg e oms@(OMS (cd, omn)) =
    if cdIsEmpty cd then f e omn
    else error $ concat [ msg, ": lookupOMS: Nonempty cd in const: "
                        , show oms]
lookupOMS _ msg _ ome =
    error $ concat [msg, ": lookupOMS: Nonsymbol: ", show ome]

toOpSymb :: (Id, OpType) -> OP_SYMB
toOpSymb (i, t) = Qual_op_name i (toOP_TYPE t) nullRange

toPredSymb :: (Id, PredType) -> PRED_SYMB
toPredSymb (i, t) = Qual_pred_name i (toPRED_TYPE t) nullRange

-- * TOPLEVEL Interface

-- | A TCSymbols is transformed to a CASL symbol with given name.
omdocToSym :: Env -> TCElement -> String -> Result Symbol
omdocToSym e sym@(TCSymbol _ ctp srole _) n =
    case srole of
      Typ | ctp == const_sort -> return $ idToSortSymbol $ nameToId n
          | otherwise -> fail $ "omdocToSym: No sorttype for " ++ show sym
      Obj -> return $
             case omdocToType e ctp of
               Left ot -> idToOpSymbol (nameToId n) ot
               Right pt -> idToPredSymbol (nameToId n) pt
      _ -> fail $ concat [ "omdocToSym: only type or object are allowed as"
                         , " symbol roles, but found: ", show srole ]

omdocToSym _ sym _ = fail $ concat [ "omdocToSym: only TCSymbol is allowed,"
                                   , " but found: ", show sym ]


omdocToSen :: Env -> TCElement -> String
           -> Result (Maybe (Named (FORMULA f)))
omdocToSen e (TCSymbol _ t sr _) n =
    case nameDecode n of
      Just _ ->
          return Nothing -- don't translate encoded names here
      Nothing ->
          let ns = makeNamed n $ omdocToFormula e t
              res b = return $ Just $ ns { isAxiom = b }
          in case sr of
               Axiom -> res True
               Theorem -> res False
               _ -> return Nothing

omdocToSen _ sym _ = fail $ concat [ "omdocToSen: only TCSymbol is allowed,"
                                   , " but found: ", show sym ]


-- | Sort generation constraints are added as named formulas.
addOMadtToTheory :: Env
                 -> (Sign f e, [Named (FORMULA f)]) -> [[OmdADT]]
                 -> Result (Sign f e, [Named (FORMULA f)])
addOMadtToTheory e (sig, nsens) adts = do
    sgcs <- mapR (omdocToSortGenConstraint e) adts
    return (sig, nsens ++ sgcs)


-- | The subsort relation is recovered from exported sentences.
addOmdocToTheory :: Env -> (Sign f e, [Named (FORMULA f)]) -> [TCElement]
                 -> Result (Sign f e, [Named (FORMULA f)])
addOmdocToTheory e (sig, nsens) tcs = do
  srel <- omdocToSortRel e tcs
  return (sig { sortRel = Rel.transClosure srel }, nsens)


-- * Algebraic Data Types

omdocToSortGenConstraint :: Env -> [OmdADT] -> Result (Named (FORMULA f))
omdocToSortGenConstraint e sortdefs = do
  -- take the last type as the type of all constraints
  let (t, cs) = mapAccumL (const $ mkConstraint e) Generated sortdefs
  -- TODO: do we take newSort or origSort?
  return $ toSortGenNamed (Sort_gen_ax cs $ t == Free) $ map newSort cs

mkConstraint :: Env -> OmdADT -> (ADTType, Constraint)
mkConstraint e (ADTSortDef nm t constrs) =
    let s = lookupSort e $ mkSimpleName nm
        l = map (mkConstructor e s) constrs
    in (t, Constraint s l s)

mkConstraint _ _ = error "mkConstraint: Malformed ADT expression"

mkConstructor :: Env -> SORT -> OmdADT -> (OP_SYMB, [Int])
mkConstructor e s (ADTConstr nm args) =
    let opn = nameToId $ lookupNotation e $ mkSimpleName nm
        l = map (mkArg e) args
    in (Qual_op_name opn (Op_type Total l s nullRange) nullRange, [0])


{- we have to create the name of this injection because we throw it away
during the export -}
mkConstructor e s (ADTInsort (_, omn)) =
    let argsort = lookupSort e omn
        opn = mkUniqueInjName argsort s
    in (Qual_op_name opn (Op_type Total [argsort] s nullRange) nullRange, [0])

mkConstructor _ _ _ = error "mkConstructor: Malformed ADT expression"

mkArg :: Env -> OmdADT -> SORT
mkArg e (ADTArg oms _) = lookupSortOMS "mkArg" e oms

mkArg _ _ = error "mkArg: Malformed ADT expression"


-- * Subsort Relation

omdocToSortRel :: Env -> [TCElement] -> Result (Rel.Rel SORT)
omdocToSortRel e = foldM (addMaybeToSortRel e) Rel.empty

addMaybeToSortRel :: Env -> Rel.Rel SORT -> TCElement -> Result (Rel.Rel SORT)
addMaybeToSortRel e r (TCSymbol n (OMA [sof, oms1, oms2]) Axiom _) =
    case nameDecode n of
      Just ("ST", _)
          | sof == const_subsortof ->
              let s1 = lookupSortOMS "addMaybeToSortRel: s1" e oms1
                  s2 = lookupSortOMS "addMaybeToSortRel: s2" e oms2
              in return $ Rel.insertKeyOrPair s1 s2 r
          | otherwise ->
              do
                warning () ("Use of subsortof in a non ST Statement: " ++ n)
                        nullRange
                return r
      _ -> return r

addMaybeToSortRel _ r _ = return r


-- * Types

omdocToType :: Env -> OMElement -> Either OpType PredType
omdocToType e (OMA (c : args)) =
    let sorts = map (lookupSortOMS "omdocToType" e) args
        opargs = init sorts
        oprange = last sorts
        res | c == const_predtype = Right $ PredType sorts
            | c == const_partialfuntype = Left $ OpType Partial opargs oprange
            | c == const_funtype = Left $ OpType Total opargs oprange
            | otherwise = error $ "omdocToType: unknown type constructor: "
                          ++ show c
    in res

omdocToType e oms@(OMS _)
    | oms == const_predtype = Right $ PredType []
    | otherwise = Left $ OpType Total [] $ lookupSortOMS "omdocToType" e oms

omdocToType _ ome = error $ "omdocToType: Non-supported element: " ++ show ome


-- * Terms and Formulas

type VarMap = Map.Map VAR SORT

type TermEnv = (Env, VarMap)

mkImplication, mkImplied, mkEquivalence
                 , mkNegation :: [FORMULA f] -> FORMULA f

mkImplication [x, y] = mkImpl x y
mkImplication _ = error "Malformed implication"
mkImplied [x, y] = mkRel RevImpl x y
mkImplied _ = error "Malformed if"
mkEquivalence [x, y] = mkEqv x y
mkEquivalence _ = error "Malformed equivalence"
mkNegation [x] = mkNeg x
mkNegation _ = error "Malformed negation"

mkDefinedness, mkExistl_equation, mkStrong_equation
    :: [TERM f] -> FORMULA f

mkDefinedness [x] = Definedness x nullRange
mkDefinedness _ = error "Malformed definedness"
mkExistl_equation [x, y] = mkExEq x y
mkExistl_equation _ = error "Malformed existl equation"
mkStrong_equation [x, y] = mkStEq x y
mkStrong_equation _ = error "Malformed strong equation"

-- Quantification, Predication and Membership are handled inside omdocToFormula

-- Term construction functions
mkT2 :: (OMElement -> a) -> (OMElement -> b) -> (a -> b -> Range -> TERM f)
     -> [OMElement] -> TERM f
mkT2 f g c l = case l of
                 [x, y] -> c (f x) (g y) nullRange
                 _ -> error "mkT2: 2 arguments expected"

mkT3 :: (OMElement -> a) -> (OMElement -> b) -> (OMElement -> c)
     -> (a -> b -> c -> Range -> TERM f) -> [OMElement] -> TERM f
mkT3 f g h c l = case l of
                   [x, y, z] -> c (f x) (g y) (h z) nullRange
                   _ -> error "mkT3: 3 arguments expected"


-- Formula construction functions
mkFF :: TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkFF e f l = f $ map (omdocToFormula' e) l

mkTF :: TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkTF e f l = f $ map (omdocToTerm' e) l

getQuantifier :: OMElement -> QUANTIFIER
getQuantifier oms
    | oms == const_forall = Universal
    | oms == const_exists = Existential
    | oms == const_existsunique = Unique_existential
    | otherwise = error $ "getQuantifier: unrecognized quantifier " ++ show oms

mkBinder :: TermEnv -> QUANTIFIER -> [OMElement] -> OMElement -> FORMULA f
mkBinder te@(e, _) q vars body =
    let (vm', vardecls) = toVarDecls te vars
        bd = omdocToFormula' (e, vm') body
    in Quantification q vardecls bd nullRange

toVarDecls :: TermEnv -> [OMElement] -> (VarMap, [VAR_DECL])
toVarDecls (e, vm) l =
    let f acc x = let (v, s) = toVarDecl e x
                      acc' = Map.insert v s acc
                  in (acc', (v, s))
        (vm', l') = mapAccumL f vm l
        -- group by same sort
        l'' = groupBy (\ x y -> snd x == snd y) l'
        -- the lists returned by groupBy are never empty, so head will succeed
        g vsl = Var_decl (map fst vsl) (snd $ head vsl) nullRange
    in (vm', map g l'')

-- in CASL we expect all bound vars to be attributed (typed)
toVarDecl :: Env -> OMElement -> (VAR, SORT)
toVarDecl e (OMATTT (OMV v) (OMAttr ct t))
    | ct == const_type = (nameToToken $ name v, lookupSortOMS "toVarDecl" e t)
    | otherwise = error $ "toVarDecl: unrecognized attribution " ++ show ct

toVarDecl _ _ = error "toVarDecl: bound variables should be attributed."

-- Toplevel entry point
omdocToFormula :: Env -> OMElement -> FORMULA f
omdocToFormula e = omdocToFormula' (e, Map.empty)


-- Functions with given VarMap

-- omdocToTerm has no toplevel entry point
omdocToTerm' :: TermEnv -> OMElement -> TERM f
omdocToTerm' e@(ie, vm) f =
    case f of
      OMA (h : args)
          | h == const_cast ->
              mkT2 (omdocToTerm' e) (lookupSortOMS "omdocToTerm: Cast" ie)
                   Cast args
          | h == const_if ->
              mkT3 (omdocToTerm' e) (omdocToFormula' e) (omdocToTerm' e)
                   Conditional args
          -- all other heads mean application
          | otherwise ->
              let os = toOpSymb $ lookupOpOMS "omdocToTerm" ie h
                  args' = map (omdocToTerm' e) args
              in Application os args' nullRange
      OMS _ -> let os = toOpSymb $ lookupOpOMS "omdocToTerm-OMS:" ie f
               in Application os [] nullRange
      OMV omn -> let var = nameToToken $ name omn
                     -- lookup the type of the variable in the varmap
                     s = Map.findWithDefault
                         (error $ concat [ "omdocToTerm': Variable not in "
                                         , "varmap: ", show var ]) var vm
                 in Qual_var var s nullRange
      OMATTT ome (OMAttr ct t)
          | ct == const_type ->
              -- same as cast
              mkT2 (omdocToTerm' e) (lookupSortOMS "omdocToTerm: Sorted" ie)
                   Sorted_term [ome, t]
          | otherwise -> error $ "omdocToTerm: unrecognized attribution "
                         ++ show ct
      _ -> error $ "omdocToTerm: no valid term " ++ show f


omdocToFormula' :: TermEnv -> OMElement -> FORMULA f
omdocToFormula' e@(ie, _) f =
    case f of
      OMA (h : args)
          | h == const_in ->
              case args of
                [x, s] ->
                    Membership (omdocToTerm' e x) (lookupSortOMS
                                                   "omdocToFormula"
                                                  ie s) nullRange
                _ -> error "Malformed membership"
          | h == const_and ->
              mkFF e conjunct args
          | h == const_or ->
              mkFF e disjunct args
          | h == const_implies ->
              mkFF e mkImplication args
          | h == const_implied ->
              mkFF e mkImplied args
          | h == const_equivalent ->
              mkFF e mkEquivalence args
          | h == const_not ->
              mkFF e mkNegation args
          | h == const_def ->
              mkTF e mkDefinedness args
          | h == const_eeq ->
              mkTF e mkExistl_equation args
          | h == const_eq ->
              mkTF e mkStrong_equation args
          -- all other heads mean predication
          | otherwise ->
              let ps = toPredSymb $ lookupPredOMS "omdocToFormula" ie h
                  g l = Predication ps l nullRange in
              mkTF e g args

      OMBIND binder args body ->
          mkBinder e (getQuantifier binder) args body

      OMS _ | f == const_true -> trueForm
            | f == const_false -> falseForm
            -- Propositional Constants (0-ary predicates):
            | otherwise ->
                Predication (toPredSymb
                             $ lookupPredOMS
                                   ("omdocToFormula: can't handle constant "
                                    ++ show f) ie f) [] nullRange
      _ -> error $ "omdocToFormula: no valid formula " ++ show f